package org.stragma.apply.modules

import scala.collection.mutable._

import org.kiama.rewriting._
import org.kiama.rewriting.Rewriter.{all,attempt,bottomup,fail,id,innermost,innermost2,not,rulefs,somebu,Strategy,Term,termToStrategy,topdown,where}

// Import the required signatures, these are obtained from running sig2scala on the Stratego signatures
import org.stragma.apply.signatures._
import org.stragma.apply.signatures.Apply._
import org.stragma.apply.signatures.Conversions._
import org.stragma.apply.signatures.Options._
import org.stragma.apply.signatures.TBase

import org.stragma.apply.modules.Options._
import org.stragma.apply.util._
import org.stragma.apply.util.LogicalOperators._
import org.stragma.apply.util.Math._
import org.stragma.apply.util.String._

import org.stragma.util.ListManager._
import org.stragma.util.Configuration._

object Normalise extends TermInputOutput {
	
	private val termMap : HashMap[TExp, scala.Int] = new HashMap[TExp, scala.Int]()
	
	/*
	 * Helper for use through Java
	 */
	def normaliseHelper(term : Term) : Term = {
		(normaliseTest(term)).get
	}

	/*
	 * This helper method executes normaliseTest n times and returns
	 * the very last result the caller
	 */
	def normaliseHelper(term : Term, n : scala.Int) : Term = {
		var result : Term = scala.None
		for(i <- 0 until n) {
			result = (normaliseTest(term)).get
			println(result)
		}
		
		return result
	}
	
	/*
	 * This helper method executes normaliseTest n times and returns
	 * the very last result to the caller
	 */
	def normaliseHelper(file : String, n : scala.Int) : Term = {
		val iTerm = loadTermFromFile(file)
		normaliseHelper(iTerm, n)
	}
	
	/*
	 * 	normalise = if get-option(|Normalise-expressions) then
     * 		canonical ; grouped ; eliminate-mul-1
	 *	else
     *		get-option(|Evaluate-constant-expressions) ; evaluate-constant-expressions
     *	end
	 */
	def normalise : Strategy = {
		if (get_config(Normalise_expressions()) == Some(true)) {
			canonical <* grouped <* eliminate_mul_1
		} else {
			if (get_config(Evaluate_constant_expressions()) == Some(true)) {
				evaluate_constant_expressions
			} else id
		}
	}
	
	def normaliseTest = canonical <* grouped <* eliminate_mul_1
			
	/*
	 * canonical sorts terms in expressions so that different multipliers
  	 * of the same term can be combined.
  	 * Canonical form:  x denotes variable, i an integer.
  	 *   x * i is canonical.
  	 *   x1 * i + x2 * j + ... is canonical if x1 alphabetically precedes x2
  	 *   e1 / e2 is canonical if e1 and e2 are canonical
  	 *      Note that division of an expression by itself with a constant multiplier may be unrecognisable if
  	 *      the parts have been made canonical    e.g. (x + y) * 2 / (x + y)  ==>  (x * 2 + y * 2) / (x * 1 + y * 1)
  	 *   x1 * x2 *... * i is a canonical product p if x1 precedes x2 alphabetically
  	 *   Canonical products are sorted by their last variable term
  	 *   Subtraction is eliminated.
  	 *   Negation is eliminated.
	 */
	def canonical = {
		// EvalKnownOther is merged in with EvalKnownTrue
		innermost(PushDownNot <+ Eliminate <+ 
			EvalAdd0 <+ EvalNeg <+ EvalExpr <+ 
			LeftGroup <+ SortExpr <+ SortTerms <+ 
			EvalKnownTrue <+ 
			NormaliseCompare <+ SortCompare <+ MergeCompare)
	}

	/*
	 * Port of strategy evaluate-constant-expressions
	 */
	def evaluate_constant_expressions : Strategy = {
		// EvalKnownOther is merged in with EvalKnownTrue
		innermost(EvalAdd0 <+ EvalNeg + EvalExpr <+ EvalKnownTrue)
	}
	
	/*
	 * grouped changes the sort order of expressions so that
  	 * they are sorted by the absolute value of the multiplier
  	 * so that terms with a common multiplier can be added together
  	 * and only one multiplication is required
	 */
	def grouped = innermost(MulAbs) <* innermost(SortMul) <* innermost(CombineMul)
	
	/*
	 * Port of strategy eliminate-mul-1
	 */
	def eliminate_mul_1 = innermost(EliminateMul1)
	
	/*
	 * Port of Strategy first-mul
	 * first-mul returns the multiplier for the first term in
  	 * a string of additions; takes the numerator of division
  	 * first-mul =
     * 		if ?Add(e1,e2) 
     *			then <first-mul>e1 
     *		else if ?Mul(e,Int(i)) 
     *    		then !i 
     *	    else if ?Div(e1,e2)
     *	        then <first-mul>e1
     *      else !"1"
     *      end
     * 	    end 
	 */
	def first_mul : Strategy = rulefs {
		case Add(e1,e2) => first_mul(e1).get
		case Mul(e,Int(i)) => i
		case Div(e1,e2) => first_mul(e1).get
		case _ => "1"
	}
	
	/*
	 * Port of NormaliseCompare Strategy
	 */
	def NormaliseCompare = rulefs {
		// Normalising comparison: first term on LHS must have +ve multiplier
 		// NormaliseCompare : |[ e != j]|           -> |[ e * -1 != -j ]|   where <first-mul>e => i; <ltS>(i,"0")
 		// NormaliseCompare : |[ e = j]|            -> |[ e * -1 = -j ]|    where <first-mul>e => i; <ltS>(i,"0")
 		// NormaliseCompare : |[ e < j]|            -> |[ e * -1 > -j ]|    where <first-mul>e => i; <ltS>(i,"0")
 		// NormaliseCompare : |[ e <= j]|           -> |[ e * -1 >= -j ]|   where <first-mul>e => i; <ltS>(i,"0")
 		// NormaliseCompare : |[ e > j]|            -> |[ e * -1 < -j ]|    where <first-mul>e => i; <ltS>(i,"0")
 		// NormaliseCompare : |[ e >= j]|           -> |[ e * -1 <= -j ]|   where <first-mul>e => i; <ltS>(i,"0")
		case Neq(e,j : Int)			if (normaliseCompareGuard(e))	=> Neq(Mul(e,Int("-1")),Neg(j))
		case Equ(e,j : Int)			if (normaliseCompareGuard(e))	=> Equ(Mul(e,Int("-1")),Neg(j))
		case Lt(e,j : Int)			if (normaliseCompareGuard(e))	=> Lt(Mul(e,Int("-1")),Neg(j))
		case Leq(e,j : Int)			if (normaliseCompareGuard(e))	=> Leq(Mul(e,Int("-1")),Neg(j))
		case Gt(e,j : Int)			if (normaliseCompareGuard(e))	=> Gt(Mul(e,Int("-1")),Neg(j))
		case Geq(e,j : Int)			if (normaliseCompareGuard(e))	=> Geq(Mul(e,Int("-1")),Neg(j))
	}
	
	/*
	 * Equivalent of where <first-mul>e => i; <ltS>(i,"0") but without a where check as this is not necessary
	 */
	private val normaliseCompareGuard = (e : TExp) => { val i = first_mul(e).get; ltS((i,"0")).isDefined }
	
	/*
	 * Port of PushDownNot rules
	 */
	def PushDownNot = rulefs {
		// Normalisation of boolean expressions
		// Canonical form is a hierarchy of and and or expressions with not expressions pushed down below
		// the and and or.
		// PushDownNot : |[ not ( e1 and e2 ) ]|  -> |[ (not e1) or (not e2) ]|
		// PushDownNot : |[ not ( e1 or e2 ) ]|   -> |[ (not e1) and (not e2) ]|
		// PushDownNot : |[ not ( e1 < e2 ) ]|    -> |[ e1 >= e2 ]|
		// PushDownNot : |[ not ( e1 <= e2 ) ]|   -> |[ e1 > e2 ]|
		// PushDownNot : |[ not ( e1 > e2 ) ]|    -> |[ e1 <= e2 ]|
		// PushDownNot : |[ not ( e1 >= e2 ) ]|   -> |[ e1 < e2 ]|
		// PushDownNot : |[ not ( e1 = e2 ) ]|    -> |[ e1 != e2 ]|
		// PushDownNot : |[ not ( e1 != e2 ) ]|   -> |[ e1 = e2 ]|
		case Not(And(e1,e2))									=> Or(Not(e1),Not(e2))
		case Not(Or(e1,e2))										=> And(Not(e1),Not(e2))
		case Not(Lt(e1,e2))										=> Geq(e1,e2)
		case Not(Leq(e1,e2))									=> Gt(e1,e2)
		case Not(Gt(e1,e2))										=> Leq(e1,e2)
		case Not(Geq(e1,e2))									=> Lt(e1,e2)
		case Not(Equ(e1,e2))									=> Neq(e1,e2)
		case Not(Neq(e1,e2))									=> Equ(e1,e2)
	}
	
	/*
	 * Port of Eliminate rules
	 */
	def Eliminate = rulefs {
		// Eliminate subtraction
		// Eliminate : |[ e1 - e2 ]|              -> |[ e1 + e2 * -1 ]|
		case Sub(e1,e2)											=> Add(e1,Mul(e2,Int("-1")))
					
		// Eliminate negation  (note: literal -1 works as Int("-1") )
		// Eliminate : |[ -e ]|                   -> |[ e * -1 ]|
		case Neg(e)												=> Mul(e,Int("-1"))
	}
	
	/*
	 * Port of LeftGroup rules
	 */
	def LeftGroup = rulefs {
		// Removing unnecessary parentheses (converting to left-associativity)
		// LeftGroup : |[ e1 + (e2 + e3) ]|        -> |[ e1 + e2 + e3 ]|
		// LeftGroup : |[ e1 * (e2 * e3) ]|        -> |[ e1 * e2 * e3 ]|
		// LeftGroup : |[ e1 and (e2 and e3) ]|    -> |[ e1 and e2 and e3 ]|
		// LeftGroup : |[ e1 or (e2 or e3) ]|      -> |[ e1 or e2 or e3 ]|
		case Add(e1,Add(e2,e3))									=> Add(Add(e1,e2),e3)
		case Mul(e1,Mul(e2,e3))									=> Mul(Mul(e1,e2),e3)
		case And(e1,And(e2,e3))									=> And(And(e1,e2),e3)
		case Or(e1,Or(e2,e3))									=> Or(Or(e1,e2),e3)
	}
	
	private def intGuard(e : TExp) = {
		e match {
			case i : Int => false
			case _ => true
		}
	}
	
	/*
	 * Port of SortExpr rules
	 */
	def SortExpr = rulefs {
		// Sorting constants to follow variables
 		// SortExpr : |[ i + e ]|                 -> |[ e + i ]|
		// SortExpr : |[ e1 + i + e2 ]|           -> |[ e1 + e2 + i ]|
		// SortExpr : |[ i * e ]|                 -> |[ e * i ]|
		// SortExpr : |[ e1 * i * e2 ]|           -> |[ e1 * e2 * i ]|
		// SortExpr : |[ e1 / i / e2 ]|           -> |[ e1 / e2 / i ]|
		case Add(i : Int,e)												=> Add(e,i)
		case Add(Add(e1,i : Int),e2) if (innermostRepeatGuard(Add(Add(e1,i),e2))) => Add(Add(e1,e2),i)
		case Mul(i : Int,e)												=> Mul(e,i)
		case Mul(Mul(e1:TExp,i:Int),e2:TExp) if (intGuard(e2))			=> Mul(Mul(e1,e2),i)
		case Div(Div(e1,i : Int),e2)									=> Div(Div(e1,e2),i)

		// Expanding multiplication
 		// SortExpr : |[ (e1 + e2) * i ]|         -> |[ e1 * i + e2 * i ]|
		case Mul(Add(e1,e2),i : Int)									=> Add(Mul(e1,i),Mul(e2,i))

		// Adding a multiplier to every expression that does not already have a muyltiplier and is not itself an addition
 		// SortExpr : |[ e1 + x + e2 ]|           -> |[ e1 + x * 1 + e2 ]|
 		// SortExpr : |[ e + x ]|                 -> |[ e + x * 1 ]|
		case Add(Add(e1,TScalarVarToTExp(TVarToTScalarVar(x : Var))),e2)=> Add(Add(e1,Mul(x,Int("1"))),e2)
		case Add(e,TScalarVarToTExp(TVarToTScalarVar(x : Var)))			=> Add(e,Mul(x,Int("1"))) 

		// Option: merge complex mutliply 
		// SortExpr : |[ e1 + e2 ]|               -> |[ e1 * 1 + e2 ]|      
		// where <not(? |[ j ]| )>e1 ; <not(? |[ e * i ]| )>e1 ; <not(? |[ e3 + e4 ]| )>e1; get-option(|Merge-complex-multiply)
		// SortExpr : |[ e1 + e2 ]|               -> |[ e1 + e2 * 1 ]|      
		// where <not(? |[ j ]| )>e2 ; <not(? |[ e * i ]| )>e2 ; <not(? |[ e3 + e4 ]| )>e2 ; get-option(|Merge-complex-multiply)
		case Add(e1:TExp,e2:TExp)	if (sortExprGuard1(e1))			=> Add(Mul(e1,Int("1")),e2)
		case Add(e1:TExp,e2:TExp)	if (sortExprGuard1(e2) && innermostRepeatGuard(Add(e1,e2)))	=> Mul(Add(e1,e2),Int("1"))
		
		// Sorting comparison expressions and evaluating numerical negation
 		// SortExpr : |[ i < e ]|                 -> |[ e > i ]|
		// SortExpr : |[ i <= e ]|                -> |[ e >= i ]|
		// SortExpr : |[ i = e ]|                 -> |[ e = i ]|
		// SortExpr : |[ i > e ]|                 -> |[ e < i ]|
		// SortExpr : |[ i >= e ]|                -> |[ e <= i ]|
		// SortExpr : |[ i != e ]|                -> |[ e != i ]|
		// SortExpr : |[ e1 + i < e2 ]|           -> |[ e1 < e2 + -i ]|
		// SortExpr : |[ e1 + i <= e2 ]|          -> |[ e1 <= e2 + -i ]|
		// SortExpr : |[ e1 + i = e2 ]|           -> |[ e1 = e2 + -i ]|
		// SortExpr : |[ e1 + i > e2 ]|           -> |[ e1 > e2 + -i ]|
		// SortExpr : |[ e1 + i >= e2 ]|          -> |[ e1 >= e2 + -i ]|
		// SortExpr : |[ e1 + i != e2 ]|          -> |[ e1 != e2 + -i ]|
		// SortExpr : |[ e1 < e2 + e3 ]|           -> |[ e1 + -e2 < e3 ]|
		// SortExpr : |[ e1 <= e2 + e3 ]|          -> |[ e1 + -e2 <= e3 ]|
		// SortExpr : |[ e1 = e2 + e3 ]|           -> |[ e1 + -e2 = e3 ]|
		// SortExpr : |[ e1 > e2 + e3 ]|           -> |[ e1 + -e2 > e3 ]|
		// SortExpr : |[ e1 >= e2 + e3 ]|          -> |[ e1 + -e2 >= e3 ]|
		// SortExpr : |[ e1 != e2 + e3 ]|          -> |[ e1 + -e2 != e3 ]|
		case Lt(i : Int,e)												=> Gt(e,i)
		case Leq(i : Int,e)												=> Geq(e,i)
		case Equ(i : Int,e)												=> Equ(e,i)
		case Gt(i : Int,e)												=> Lt(e,i)
		case Geq(i : Int,e)												=> Leq(e,i)
		case Neq(i : Int,e)												=> Neq(e,i)
		case Lt(Add(e1,i : Int),e2)										=> Lt(e1,Add(e2,Neg(i)))
		case Leq(Add(e1,i : Int),e2)									=> Leq(e1,Add(e2,Neg(i))) 
		case Equ(Add(e1,i : Int),e2)									=> Equ(e1,Add(e2,Neg(i)))
		case Gt(Add(e1,i : Int),e2)										=> Gt(e1,Add(e2,Neg(i)))
		case Geq(Add(e1,i : Int),e2)									=> Geq(e1,Add(e2,Neg(i)))
		case Neq(Add(e1,i : Int),e2)									=> Neq(e1,Add(e2,Neg(i)))
		case Lt(e1,Add(e2,e3))											=> Lt(Add(e1,Neg(e2)),e3)
		case Leq(e1,Add(e2,e3))											=> Leq(Add(e1,Neg(e2)),e3)
		case Equ(e1,Add(e2,e3))											=> Equ(Add(e1,Neg(e2)),e3)
		case Gt(e1,Add(e2,e3))											=> Gt(Add(e1,Neg(e2)),e3)
		case Geq(e1,Add(e2,e3))											=> Geq(Add(e1,Neg(e2)),e3)
		case Neq(e1,Add(e2,e3))											=> Neq(Add(e1,Neg(e2)),e3)

		// Introduce compare with zero
 		// SortExpr : |[ e1 < e2 ]|           -> |[ e1 + -e2 < 0 ]|   where <not(?Int(i))>e2
 		// SortExpr : |[ e1 <= e2 ]|          -> |[ e1 + -e2 <= 0 ]|  where <not(?Int(i))>e2
 		// SortExpr : |[ e1 = e2 ]|           -> |[ e1 + -e2 = 0 ]|   where <not(?Int(i))>e2
 		// SortExpr : |[ e1 > e2 ]|           -> |[ e1 + -e2 > 0 ]|   where <not(?Int(i))>e2
 		// SortExpr : |[ e1 >= e2 ]|          -> |[ e1 + -e2 >= 0 ]|  where <not(?Int(i))>e2
 		// SortExpr : |[ e1 != e2 ]|          -> |[ e1 + -e2 != 0 ]|  where <not(?Int(i))>e2

		// NOTE: As scala is strongly typed the guards below are not necessary, I have kept them
		// there for readability
		case Lt(e1,e2) 			if (sortExprGuard(e2) == true) 			=> Lt(Add(e1,Neg(e2)),Int("0"))
		case Leq(e1,e2)			if (sortExprGuard(e2) == true)			=> Leq(Add(e1,Neg(e2)),Int("0"))
		case Equ(e1,e2)			if (sortExprGuard(e2) == true)			=> Equ(Add(e1,Neg(e2)),Int("0"))
		case Gt(e1,e2)			if (sortExprGuard(e2) == true)			=> Gt(Add(e1,Neg(e2)),Int("0"))
		case Geq(e1,e2)			if (sortExprGuard(e2) == true)			=> Geq(Add(e1,Neg(e2)),Int("0"))
		case Neq(e1,e2)			if (sortExprGuard(e2) == true)			=> Neq(Add(e1,Neg(e2)),Int("0"))
		case e 															=> fail// Do nothing
	}
	
	/*
	 * Used by the SortExpr rules as part of a conditional guard
	 */
	private val sortExprGuard = (e2 : TExp) => {
		where(not(rulefs { case Int(_) => id }))(e2).isDefined 	// isDefined is used to convert the Option result into a Boolean
	}
	
	private val sortExprGuard1 = (e2 : TExp) => {
		// The last not for Func is a bit of hack
		(where(
			not(rulefs { case Int(_) => id }) <* 
			not(rulefs { case Mul(e,i : Int) => id }) <* 
			not(rulefs { case Add(e3,e4) => id }) <*
			not(rulefs { case TScalarVarToTExp(Func(e5,e6)) => id })))(e2).isDefined
	}
	
	/**
	 * This guard is required because the strategy sortExpr when used with a strategy such as innermost
	 * can produce and infinite loop
	 */
	private def innermostRepeatGuard (term : TExp) : Boolean = {
		if (termMap.contains (term)) {
			termMap (term) = termMap (term) + 1
			if (termMap (term) > 10)
				false
			else
				true
		}
		else {
			termMap += (term) -> 1
			true
		}
	}
	
	/*
	 * Port of strategy
	 * Sorting variable names first in alphabetic order then expressions
  	 * Exception: sort the words row and column ahead of all other words
  	 * (this is so that expressions involving row and column have a consistent beautified form)
  	 * variable-name-reorder =
     * if ?(_,"row") then id else
     * if ?("row",_) then fail else
     * if ?(_,"column") then id else
     * if ?("column",_) then fail else
     * string-gt
     * end end end end
	 */
	def variable_name_reorder =	rulefs {
		case (_,"row") => id
		case ("row",_) => fail
		case (_,"column") => id
		case ("column",_) => fail
		case (a:String,b:String) =>
			string_gt(a,b)
	}
	
	/*
	 * Port of is-comparison rules
	 */
	def is_comparison = rulefs {
		// is-comparison succeeds if the node is a comparison, and returns the 
 		// sort order number for the comparison type and the LHS expression
 		// is-comparison : |[ e < i ]|  -> ("1",e)
 		// is-comparison : |[ e <= i ]| -> ("2",e)
 		// is-comparison : |[ e = i ]|  -> ("3",e)
 		// is-comparison : |[ e >= i ]| -> ("4",e)
 		// is-comparison : |[ e > i ]|  -> ("5",e)
 		// is-comparison : |[ e != i ]| -> ("0",e)
		case Lt(e,i : Int) => ("1",e)
		case Leq(e,i : Int) => ("2",e)
		case Equ(e,i : Int) => ("3",e)
		case Geq(e,i : Int) => ("4",e)
		case Gt(e,i : Int) => ("5",e)
		case Neq(e,i : Int) => ("0",e) 
	}
	
	/*
	 * Port of Strategy Sort Terms
	 * If the first expression is not canonical, swap it.  If it is canonical, it will either be sum 
	 * of canonical terms or a single canonical term.
  	 * SortTerms : Add(e1,e2)                  -> Add(e2,e1)        
     *         where   <not(?Add(_,_))>e1
     *               ; <not(?Mul(Var(_),Int(_)))>e1
     *               ; <?Mul(Var(_),Int(_))>e2
  	 * If the middle expression is not a canonical term, swap it
  	 *	SortTerms : Add(Add(e1,e2),e3)          -> Add(Add(e1,e3),e2) 
     *         where   <not(?Mul(Var(_),Int(_)))>e2
     *               ; <?Mul(Var(_),Int(_))>e3
	 */
	def SortTerms =	rulefs {
		// Note that a + b + c is really +(+(a b) c) so the two rules below handle sorting in every possible case.
 		// SortTerms : |[ x1 * i + x2 * j ]|       -> |[ x2 * j + x1 * i ]|     where <variable-name-reorder>(x1,x2)
 		// SortTerms : |[ e + x1 * i + x2 * j ]|   -> |[ e + x2 * j + x1 * i ]| where <variable-name-reorder>(x1,x2)
		case Add(Mul(TScalarVarToTExp(TVarToTScalarVar(Var(x1))),i),Mul(TScalarVarToTExp(TVarToTScalarVar(Var(x2))),j))
			if(variable_name_reorder(x1,x2).isDefined) => Add(Mul(Var(x2),j),Mul(Var(x1),i))

		case Add(Add(e, Mul(TScalarVarToTExp(TVarToTScalarVar(Var(x1))),i)),Mul(TScalarVarToTExp(TVarToTScalarVar(Var(x2))),j))
			if(variable_name_reorder(x1,x2).isDefined) => Add(Add(e,Mul(Var(x2),j)),Mul(Var(x1),i))
			
		case Add(Add(e1,e2),e3) 
			if(sortTermsGuard2(e2,e3) == true) => Add(Add(e1,e3),e2)
			
		case Add(e1,e2) 
			if(sortTermsGuard1(e1,e2) == true ) => Add(e2,e1)
	}
	
	private def matchMulStrat = rulefs { 
		case Mul(TScalarVarToTExp(TVarToTScalarVar(Var(_))),Int(_)) => id 
	}
	
	/*
	 * Used by the SortTerms conditional guards
	 */
	private val sortTermsGuard1 = (e1:TExp,e2:TExp) => {
		
		def matchAddStrat = rulefs { 
				case Add(_,_) => id 
		}
		
		if ((where(not(matchAddStrat)) <* where(not(matchMulStrat)))(e1).isDefined) {
			if (matchMulStrat(e2).isDefined) 
				true
			else
				false
		}
		else
			false
	}
	
	/*
	 * Used by the SortTerms conditional guards
	 */
	private val sortTermsGuard2 = (e2:TExp,e3:TExp) => {
		var state = false
		if ((where(not(matchMulStrat))(e2)).isDefined) {
			if ((where(matchMulStrat)(e3)).isDefined) {
				state = true
			} else
				state = false
		}
			
		state
	}
	
	/*
	 * Port of strategy
	 * Sorting of comparison terms.  The terms must be canonical first, with expressions on LHS and
  	 * integer on RHS.
  	 * Sort to group together the same comparison variables with the same direction of comparison
  	 * Sort first on the basis of the left-most differing variable, then on the basis of direction
  	 * of comparison  < <= = >= >.
  	 * comparison-reorder =
     * Calculate the 'code' - true for reorder, false for correct order, fail for unknown
     * Only actually reorder if the 'code' is true.
     * comparison-reorder-code ; ?True
	 */
	def comparison_reorder = comparison_reorder_code <* rulefs { 
		case True() => id 
		case _ => fail
	}
	
	/*
	 * Port of comparison-reorder-code strategy
	 */
	def comparison_reorder_code : Strategy = rulefs {
			// Checking for unequal expressions 
      		// case ?(e,e) : fail
			case (e1:TBase,e2:TBase) if (e1==e2) => fail
			
			// Comparing variable names
      		// case ?(Mul(Var(x1),Int(_)),Mul(Var(x2),Int(_))) : <variable-name-reorder>(x1,x2) < !True + !False 
      		// case ?(Var(x3),Var(x4)) : <variable-name-reorder>(x3,x4) < !True + !False
			case (Mul(TScalarVarToTExp(TVarToTScalarVar(Var(x1))),Int(_)),Mul(TScalarVarToTExp(TVarToTScalarVar(Var(x2))),Int(_))) 
					=> if (variable_name_reorder(x1,x2) == Some(x1,x2)) True() else False()
			case (Var(x3),Var(x4))
					=> if (variable_name_reorder(x3,x4) == Some(x3,x4)) True() else False()
					
			 // Checking for things to look inside of
      		 // case ?(Add(e1,e2),Add(e3,e4)) : <comparison-reorder-code>(e1,e3) <+ <comparison-reorder-code>(e2,e4) 
      		 // case ?(Mul(e7,e8),Mul(e9,e10)) : <comparison-reorder-code>(e7,e9) <+ <comparison-reorder-code>(e8,e10) 
      		 // case ?(Neg(e5),Neg(e6)) : <comparison-reorder-code>(e5,e6) 
			case (Add(e1,e2),Add(e3,e4)) 
				=> (comparison_reorder_code((e1,e3)).get) <+ (comparison_reorder_code((e2,e4)).get)
			case (Mul(e7,e8),Mul(e9,e10))
				=> (comparison_reorder_code((e7,e8)).get) <+ (comparison_reorder_code((e8,e10)).get)
			case (Neg(e5),Neg(e6))
				=> comparison_reorder_code(e5,e6).get
				
			 // If a non-matching structure, compare LHS but if it matches, make a consistent structure-based decision
      		// case ?(Add(a1,a2),a3) : <comparison-reorder-code>(a1,a3) <+ !True
      		// case ?(a4,Add(a5,a6)) : <comparison-reorder-code>(a4,a5) <+ !False
      		// case ?(Mul(m1,m2),m3) : <comparison-reorder-code>(m1,m3) <+ !True
      		// case ?(m4,Mul(m5,m6)) : <comparison-reorder-code>(m4,m5) <+ !False
      		// case ?(Neg(n1),n2)    : <comparison-reorder-code>(n1,n2) <+ !True
      		// case ?(n3,Neg(n4))    : <comparison-reorder-code>(n3,n4) <+ !False
			case (Add(a1,a2),a3)
				=> (comparison_reorder_code <+ trueStrategy)(a1,a3).get
			case (a4,Add(a5,a6))
				=> (comparison_reorder_code<+ falseStrategy)(a4,a5).get
			case (Mul(m1,m2),m3)
				=> (comparison_reorder_code <+ trueStrategy)(m1,m3).get
			case (m4,Mul(m5,m6))
				=> (comparison_reorder_code <+ falseStrategy)(m4,m5).get
			case (Neg(n1),n2)
				=> (comparison_reorder_code <+ trueStrategy)(n1,n2).get
			case (n3,Neg(n4))
				=> (comparison_reorder_code <+ falseStrategy)(n3,n4).get
			
			case (a,b) =>
				// println("a->" + a)
				// println("b->" + b)
				// println("is_comparison(a)->" + is_comparison(a))
				is_comparison(a) match {
					case Some((ac : String,aleft)) =>
						// println("ac->" + ac)
						// println("aleft->" + aleft)
						is_comparison(b) match {
							case Some((bc : String,bleft)) =>
								// println("bc->" + bc)
								// println("bleft->" + bleft)
								val leqSRes = leqS(Int(ac),Int(bc))
								val strat = rulefs {
									case _ => if (leqSRes.isDefined) False() else True()
								}
								// println("leqSRes->" + leqSRes)
								(comparison_reorder_code <+ strat)(aleft,bleft).get
							case _ =>
								True()
						}
					case _ =>
						// println("is_comparison(b)->" + is_comparison(b))
						is_comparison(b) match {
							case Some((c,d)) => False()
							case _ => fail
						}
				}
		}
	
	/*
	 * Port of the SortCompare rules
	 */
	def SortCompare = rulefs {
		// SortCompare : |[ e1 and e2 ]|          -> |[ e2 and e1 ]|         where <comparison-reorder>(e1,e2)
 		// SortCompare : |[ e1 and e2 and e3 ]|   -> |[ e1 and e3 and e2 ]|  where <comparison-reorder>(e2,e3)
 		// SortCompare : |[ e1 or e2 ]|           -> |[ e2 or e1 ]|          where <comparison-reorder>(e1,e2)
 		// SortCompare : |[ e1 or e2 or e3 ]|     -> |[ e1 or e3 or e2 ]|    where <comparison-reorder>(e2,e3)
		case And(And(e1,e2),e3) if (comparison_reorder_code(e2,e3) == Some(True())) 		=> And(And(e1,e3),e2)
		case And(e1,e2) if (comparison_reorder_code(e1,e2) == Some(True())) 				=> And(e2,e1)
		case Or(Or(e1,e2),e3) if (comparison_reorder_code(e2,e3) == Some(True())) 			=> Or(Or(e1,e3),e2)
		case Or(e1,e2) if (comparison_reorder_code(e1,e2) == Some(True())) 					=> Or(e2,e1)
	}
	
	/*
	 * Port of MergeCompare rules from Normalise
	 */
	def MergeCompare = rulefs {
			// MergeCompare : |[ e < i and e < j ]|   -> |[ e < k ]|             where <minstring>(i,j) => k
  			// MergeCompare : |[ e < i and e <= j ]|  -> |[ e <= j ]|            where <gtS>(i,j)
  			// MergeCompare : |[ e < i and e <= j ]|  -> |[ e < i ]|             where <leqS>(i,j)
  			// MergeCompare : |[ e <= i and e <= j ]| -> |[ e <= k ]|            where <minstring>(i,j) => k
  			// MergeCompare : |[ e = i and e = j ]|   -> |[ false ]|             where <not(eq)>(i,j)
  			// MergeCompare : |[ e = i and e = i ]|   -> |[ e = i ]|
  			// MergeCompare : |[ e >= i and e >= j ]| -> |[ e >= k ]|            where <maxstring>(i,j) => k
  			// MergeCompare : |[ e >= i and e > j ]|  -> |[ e >= i ]|            where <gtS>(i,j)
  			// MergeCompare : |[ e >= i and e > j ]|  -> |[ e > j ]|             where <leqS>(i,j)
  			// MergeCompare : |[ e > i and e > j ]|   -> |[ e > k ]|             where <maxstring>(i,j) => k
			case And(Lt(e1,i : Int),Lt(e2,j : Int)) 		if (e1==e2)								=> Lt(e1,minstring(i,j))
			case And(Lt(e1,i : Int),Leq(e2,j : Int)) 		if (e1==e2 && gtS(i,j).isDefined)		=> Leq(e1,j)
			case And(Lt(e1,i : Int),Leq(e2,j : Int)) 		if (e1==e2 && leqS(i,j).isDefined)		=> Lt(e1,i)
			case And(Leq(e1,i : Int),Leq(e2,j : Int)) 		if (e1==e2)								=> Leq(e1,minstring(i,j))
			case And(Equ(e1,i: Int),Equ(e2,j : Int)) 		if (e1==e2 && neq(i,j).isDefined)		=> False()
			case And(Equ(e1,i: Int),Equ(e2,j : Int)) 		if (e1==e2 && i==j)						=> Equ(e1,i)
			case And(Geq(e1,i : Int),Geq(e2,j : Int)) 		if (e1==e2)								=> Geq(e1,maxstring(i,j))
			case And(Geq(e1,i : Int),Gt(e2,j : Int)) 		if (e1==e2 && gtS(i,j).isDefined)		=> Geq(e1,i)
			case And(Geq(e1,i : Int),Gt(e2,j : Int)) 		if (e1==e2 && leqS(i,j).isDefined)		=> Gt(e1,j)
			case And(Gt(e1,i : Int),Gt(e2,j : Int)) 		if (e1==e2)								=> Gt(e1,maxstring(i,j))
			
			// MergeCompare : |[ e1 and e < i and e < j ]|   -> |[ e1 and e < k ]|             where <minstring>(i,j) => k
  			// MergeCompare : |[ e1 and e < i and e <= j ]|  -> |[ e1 and e <= j ]|            where <gtS>(i,j)
  			// MergeCompare : |[ e1 and e < i and e <= j ]|  -> |[ e1 and e < i ]|             where <leqS>(i,j)
  			// MergeCompare : |[ e1 and e <= i and e <= j ]| -> |[ e1 and e <= k ]|            where <minstring>(i,j) => k
  			// MergeCompare : |[ e1 and e = i and e = j ]|   -> |[ false ]|                    where <not(eq)>(i,j)
  			// MergeCompare : |[ e1 and e = i and e = i ]|   -> |[ e1 and e = i ]|
  			// MergeCompare : |[ e1 and e >= i and e >= j ]| -> |[ e1 and e >= k ]|            where <maxstring>(i,j) => k
  			// MergeCompare : |[ e1 and e >= i and e > j ]|  -> |[ e1 and e >= i ]|            where <gtS>(i,j)
  			// MergeCompare : |[ e1 and e >= i and e > j ]|  -> |[ e1 and e > j ]|             where <leqS>(i,j)
  			// MergeCompare : |[ e1 and e > i and e > j ]|   -> |[ e1 and e > k ]|             where <maxstring>(i,j) => k
			case And(And(e,Lt(e1,i : Int)),Lt(e2,j : Int)) 	if (e1==e2)								=> And(e,Lt(e1,minstring(i,j)))
			case And(And(e,Lt(e1,i : Int)),Leq(e2,j : Int)) if (e1==e2 && gtS(i,j).isDefined)		=> And(e,Leq(e1,j))
			case And(And(e,Lt(e1,i : Int)),Leq(e2,j : Int)) if (e1==e2 && leqS(i,j).isDefined)		=> And(e,Lt(e1,i))
			case And(And(e,Leq(e1,i : Int)),Leq(e2,j : Int)) if (e1==e2)							=> And(e,Leq(e1,minstring(i,j)))
			case And(And(e,Equ(e1,i: Int)),Equ(e2,j : Int)) if (e1==e2 && neq(i,j).isDefined)		=> False()
			case And(And(e,Equ(e1,i: Int)),Equ(e2,j : Int)) if (e1==e2 && i==j)						=> And(e,Equ(e1,i))
			case And(And(e,Geq(e1,i : Int)),Geq(e2,j : Int)) if (e1==e2)							=> And(e,Geq(e1,maxstring(i,j)))
			case And(And(e,Geq(e1,i : Int)),Gt(e2,j : Int)) if (e1==e2 && gtS(i,j).isDefined)		=> And(e,Geq(e1,i))
			case And(And(e,Geq(e1,i : Int)),Gt(e2,j : Int)) if (e1==e2 && leqS(i,j).isDefined)		=> And(e,Gt(e1,j))
			case And(And(e,Gt(e1,i : Int)),Gt(e2,j : Int)) 	if (e1==e2)								=> And(e,Gt(e1,maxstring(i,j)))
			
			// MergeCompare : |[ e < i or e < j ]|   -> |[ e < k ]|             where <maxstring>(i,j) => k
  			// MergeCompare : |[ e < i or e <= j ]|  -> |[ e <= j ]|            where <leqS>(i,j)
  			// MergeCompare : |[ e < i or e <= j ]|  -> |[ e < i ]|             where <gtS>(i,j)
  			// MergeCompare : |[ e <= i or e <= j ]| -> |[ e <= k ]|            where <maxstring>(i,j) => k
  			// MergeCompare : |[ e = i or e = i ]|   -> |[ e = i ]|
  			// MergeCompare : |[ e >= i or e >= j ]| -> |[ e >= k ]|            where <minstring>(i,j) => k
  			// MergeCompare : |[ e >= i or e > j ]|  -> |[ e >= i ]|            where <leqS>(i,j)
  			// MergeCompare : |[ e >= i or e > j ]|  -> |[ e > j ]|             where <gtS>(i,j)
  			// MergeCompare : |[ e > i or e > j ]|   -> |[ e > k ]|             where <minstring>(i,j) => k
			case Or(Lt(e1,i : Int),Lt(e2,j : Int)) 			if (e1==e2)								=> Lt(e1,maxstring(i,j))
			case Or(Lt(e1,i : Int),Leq(e2,j : Int)) 		if (e1==e2 && leqS(i,j).isDefined)		=> Leq(e1,j)
			case Or(Lt(e1,i : Int),Leq(e2,j : Int)) 		if (e1==e2 && gtS(i,j).isDefined)		=> Lt(e1,i)
			case Or(Leq(e1,i : Int),Leq(e2,j : Int)) 		if (e1==e2)								=> Leq(e1,maxstring(i,j))
			case Or(Equ(e1,i: Int),Equ(e2,j : Int)) 		if (e1==e2 && i==j)						=> Equ(e1,i)
			case Or(Geq(e1,i : Int),Geq(e2,j : Int)) 		if (e1==e2)								=> Geq(e1,minstring(i,j))
			case Or(Geq(e1,i : Int),Gt(e2,j : Int)) 		if (e1==e2 && leqS(i,j).isDefined)		=> Geq(e1,i)
			case Or(Geq(e1,i : Int),Gt(e2,j : Int)) 		if (e1==e2 && gtS(i,j).isDefined)		=> Gt(e1,j)
			case Or(Gt(e1,i : Int),Gt(e2,j : Int)) 			if (e1==e2)								=> Gt(e1,minstring(i,j))
			
			// MergeCompare : |[ e1 or e < i or e < j ]|   -> |[ e1 or e < k ]|             where <maxstring>(i,j) => k
  			// MergeCompare : |[ e1 or e < i or e <= j ]|  -> |[ e1 or e <= j ]|            where <leqS>(i,j)
  			// MergeCompare : |[ e1 or e < i or e <= j ]|  -> |[ e1 or e < i ]|             where <gtS>(i,j)
  			// MergeCompare : |[ e1 or e <= i or e <= j ]| -> |[ e1 or e <= k ]|            where <maxstring>(i,j) => k
  			// MergeCompare : |[ e1 or e = i or e = i ]|   -> |[ e1 or e = i ]|
  			// MergeCompare : |[ e1 or e >= i or e >= j ]| -> |[ e1 or e >= k ]|            where <minstring>(i,j) => k
  			// MergeCompare : |[ e1 or e >= i or e > j ]|  -> |[ e1 or e >= i ]|            where <leqS>(i,j)
  			// MergeCompare : |[ e1 or e >= i or e > j ]|  -> |[ e1 or e > j ]|             where <gtS>(i,j)
  			// MergeCompare : |[ e1 or e > i or e > j ]|   -> |[ e1 or e > k ]|             where <minstring>(i,j) => k
			case Or(Or(e,Lt(e1,i : Int)),Lt(e2,j : Int)) 	if (e1==e2)								=> Or(e,Lt(e1,maxstring(i,j)))
			case Or(Or(e,Lt(e1,i : Int)),Leq(e2,j : Int)) 	if (e1==e2 && leqS(i,j).isDefined)		=> Or(e,Leq(e1,j))
			case Or(Or(e,Lt(e1,i : Int)),Leq(e2,j : Int)) 	if (e1==e2 && gtS(i,j).isDefined)		=> Or(e,Lt(e1,i))
			case Or(Or(e,Leq(e1,i : Int)),Leq(e2,j : Int)) 	if (e1==e2)								=> Or(e,Leq(e1,maxstring(i,j)))
			case Or(Or(e,Equ(e1,i: Int)),Equ(e2,j : Int)) 	if (e1==e2 && i==j)						=> Or(e,Equ(e1,i))
			case Or(Or(e,Geq(e1,i : Int)),Geq(e2,j : Int)) 	if (e1==e2)								=> Or(e,Geq(e1,minstring(i,j)))
			case Or(Or(e,Geq(e1,i : Int)),Gt(e2,j : Int)) 	if (e1==e2 && leqS(i,j).isDefined)		=> Or(e,Geq(e1,i))
			case Or(Or(e,Geq(e1,i : Int)),Gt(e2,j : Int)) 	if (e1==e2 && gtS(i,j).isDefined)		=> Or(e,Gt(e1,j))
			case Or(Or(e,Gt(e1,i : Int)),Gt(e2,j : Int)) 	if (e1==e2)								=> Or(e,Gt(e1,minstring(i,j)))
		}
	
	/*
	 * Port of rule
	 * Evaluating negation
  	 * EvalNeg : |[ -i ]|                     -> |[ k ]|           where <subtS>("0",i) => k
	 */
	def EvalNeg = rulefs {
		case Neg(i : Int)			=> subtS(Int("0"), i)
	}
	
	/*
	 * Simplification of identities and zeroes
	 * EvalAdd0 : |[ e + 0 ]|           -> |[ e ]|
	 * EvalAdd0 : |[ 0 + e ]|           -> |[ e ]|
	 */
	def EvalAdd0 = rulefs {
		case Add(e, Int("0"))		=> e
		case Add(Int("0"), e)		=> e
	}
	
	/*
	 * Port Of Rule (NOTE: In scala because of the way pattern matching works we do not need to define EvalKnownOther)
	 * Evaluate @known(c): If c is true then return true, else return false
  	 * EvalKnownTrue : |[ @known(true) ]|  -> |[ true ]|
  	 * EvalKnownOther : |[ @known(e) ]|    -> |[ false ]|
	 */
	def EvalKnownTrue = rulefs {
		case Known(True())			=> True()
		case Known(e)				=> False()
	}

	/*
	 * Port of all the EvalExpr Rules
	 */
	def EvalExpr = rulefs {
		  	// Evaluating sums and differences of integers
			// EvalExpr : |[ i + j ]|                 -> |[ k ]|           where <addS>(i,j) => k
  	 		// EvalExpr : |[ e + i + j ]|             -> |[ e + k ]|       where <addS>(i,j) => k
			case Add(i : Int,j : Int)															=> addS(i,j)
			case Add(Add(e : Int, i : Int),j : Int)												=> Add(e,addS(i,j))
			
			// Evaluating multiplication
			// EvalExpr : |[ i * j ]|                 -> |[ k ]|           where <mulS>(i,j) => k
  	 		// EvalExpr : |[ e * i * j ]|             -> |[ e * k ]|       where <mulS>(i,j) => k
  	 		// EvalExpr : |[ e1 / e2 * -1 ]|          -> |[ e1 * -1 / e2 ]|
			case Mul(i : Int,j : Int)															=> mulS(i,j)
			case Mul(Mul(e : Int,i : Int),j : Int)												=> Mul(e,mulS(i,j))
			case Mul(Div(e1 : Int, e2 : Int),Int("-1"))											=> Div(Mul(e1,Int("-1")),e2)
			
		  	// Evaluating division if the division is exact
			// EvalExpr : |[ i  / j ]|                -> |[ k ]|           where <modS>(i,j) => "0"; <divS>(i,j) => k
  	 		// EvalExpr : |[ e * i  / j ]|            -> |[ e * k ]|       where <modS>(i,j) => "0"; <divS>(i,j) => k
			case Div(i : Int,j : Int) if modS(i,j) == Int("0")									=> divS(i,j)
			case Div(Mul(e : Int,i : Int),j : Int) if modS(i,j) == Int("0") 					=> Mul(e,divS(i,j))
			
			// Extracting constants from inside multiplication
			// EvalExpr : |[ (e + i) * j ]|           -> |[ e * j + k ]|   where <mulS>(i,j) => k
			case Mul(Add(e : Int,i : Int),j : Int) 												=> Add(Mul(e,j),addS(i,j))
			
			// Combining multiplication terms
  			// These rules work best when we sort the similar terms together
			// EvalExpr : |[ e * i + e * j ]|         -> |[ e * k ]|       where <addS>(i,j) => k
  	 		// EvalExpr : |[ e1 + e * i + e * j ]|    -> |[ e1 + e * k ]|  where <addS>(i,j) => k
			case Add(Mul(e1 : Int,i : Int),Mul(e2 : Int,j : Int)) if (e1==e2) 					=> Mul(e1,addS(i,j))
			case Add(Add(e1 : Int, Mul(e2 : Int,i : Int)),Mul(e3 : Int,j : Int)) if (e2==e3) 	=> Add(e1,Mul(e2,addS(i,j)))
			
			// Dividing the expression by itself
			// EvalExpr : |[ e / e ]|                 -> |[ 1 ]|
  	 		// EvalExpr : |[ e * i / e ]|             -> |[ i ]|
  	 		// EvalExpr : |[ e / (e * i) ]|           -> |[ 1 / i ]|
  	 		// EvalExpr : |[ e * i / (e * j) ]|       -> |[ i / j ]|
			case Div(e1 : Int,e2 : Int) if (e1==e2)												=> Int("1")
			case Div(Mul(e1 : Int,i : Int),e2 : Int) if (e1==e2)								=> i
			case Div(e1 : Int, Mul(e2 : Int,i : Int)) if (e1==e2)								=> Div(Int("1"),i)
			case Div(Mul(e1 : Int,i : Int),Mul(e2 : Int,j : Int)) 	if(e1==e2) 					=> Div(i,j)
			
			// Evaluating division
			// EvalExpr : |[ i / j ]|                 -> |[ k ]|           where <divS>(i,j) => k
  	 		// EvalExpr : |[ e / i / j ]|             -> |[ e / k ]|       where <mulS>(i,j) => k
  	 		// EvalExpr : |[ i % j ]|                 -> |[ k ]|           where <modS>(i,j) => k
			case Div(i : Int,j : Int)															=> divS(i,j)
			case Div(Div(e : Int, i : Int), j : Int) 											=> Div(e,mulS(i,j))
			case Mod(i : Int,j : Int)															=> modS(i,j)
			
			// Note: Unlike the Stratego functions the Scala calls below do not use a wrapper
			// called compare, this is because the comparative check is built into each
			// function call, i.e. ltS, gtS etc do the comparative, this makes a call to compare
			// redundant.
			// EvalExpr : |[ i < j ]|                 -> <compare(ltS)>(i,j)
	 		// EvalExpr : |[ i > j ]|                 -> <compare(gtS)>(i,j)
	 		// EvalExpr : |[ i <= j ]|                -> <compare(leqS)>(i,j)
	 		// EvalExpr : |[ i >= j ]|                -> <compare(geqS)>(i,j)
	 		// EvalExpr : |[ i = j ]|                 -> <compare(eq)>(i,j)
	 		// EvalExpr : |[ i != j ]|                -> <compare(not(eq))>(i,j)
			case Lt(i : Int, j : Int)								=> if (ltS(i,j).isDefined) ltS(i,j).get else fail
			case Gt(i : Int, j : Int)								=> if (gtS(i,j).isDefined) gtS(i,j).get else fail
			case Leq(i : Int, j : Int)								=> if (leqS(i,j).isDefined) leqS(i,j).get else fail
			case Geq(i : Int, j : Int)								=> if (geqS(i,j).isDefined) geqS(i,j).get else fail
			case Equ(i : Int, j : Int)								=> if (eqS(i,j).isDefined) eqS(i,j).get else fail
			case Neq(i : Int, j : Int)								=> if (neq(i,j).isDefined) neq(i,j).get else fail
			
		  	// simplification of identities and zeroes
			// EvalExpr : |[ e / 1 ]|           -> |[ e ]|
  	 		// EvalExpr : |[ e * 0 ]|           -> |[ 0 ]|
  	 		// EvalExpr : |[ 0 * e ]|           -> |[ 0 ]|
  	 		// EvalExpr : |[ 0 / e ]|           -> |[ 0 ]|
  	 		// EvalExpr : |[ true or e ]|       -> |[ true ]|
  	 		// EvalExpr : |[ e or true ]|       -> |[ true ]|
  	 		// EvalExpr : |[ e or false ]|      -> |[ e ]|
  	 		// EvalExpr : |[ false or e ]|      -> |[ e ]|
  	 		// EvalExpr : |[ e and true ]|      -> |[ e ]|
  	 		// EvalExpr : |[ true and e ]|      -> |[ e ]|
  	 		// EvalExpr : |[ e and false ]|     -> |[ false ]|
  	 		// EvalExpr : |[ false and e ]|     -> |[ false ]|
			case Div(e, Int("1"))									=> e
			case Mul(e, Int("0"))									=> Int("0")
			case Mul(Int("0"), e)									=> Int("0")
			case Div(Int("0"), e)									=> Int("0")
			case Or(True(),e) 										=> True()
			case Or(e,True())										=> True()
			case Or(e,False())										=> e
			case Or(False(),e)										=> e
			case And(e,True())										=> e
			case And(True(),e)										=> e
			case And(False(),e)										=> False()
			case And(e,False())										=> False()
			
			// boolean negation
  	 		// EvalExpr : |[ not true ]|        -> |[ false ]|
  	 		// EvalExpr : |[ not false ]|       -> |[ true ]|
  	 		// EvalExpr : |[ not not e ]|       -> |[ e ]|
			case Not(True())										=> False()
			case Not(False())										=> True()
			case Not(Not(e))										=> e
			
			// EvalExpr : IfElseExp(False(), x, y)   -> y
  	 		// EvalExpr : IfElseExp(True(), x, y)    -> x
			case IfElseExp(False(),x,y)								=> y
			case IfElseExp(True(),x,y)								=> x
		}

	/*
	 * Port of MulAbs rule
	 */
	def MulAbs = rulefs {
		// Convert all multipliers to positive terms
 		// MulAbs : |[ e * i ]|                 -> |[ -e * j ]|  where <ltS>(i,"0"); <subtS>("0",i) => j
		case Mul(TScalarVarToTExp(TVarToTScalarVar(e : Var)),i : Int)
			if (ltS(i,Int("0")).isDefined)
				=> 	Mul(Neg(e),subtS(Int("0"),i))
	}
	
	/*
	 * Port of SortMul rules
	 */
	def SortMul = rulefs {
		 // Sort multipliers numerically
 	 	// It is faster on the PC using gcc to sort larger multipliers last
 	 	// SortMul : |[ e1 * i + e2 * j ]|      -> |[ e2 * j + e1 * i ]|       where <ltS>(j,i)
 	 	// SortMul : |[ e + e1 * i + e2 * j ]|  -> |[ e + e2 * j + e1 * i ]|   where <ltS>(j,i)
		case Add(Mul(TScalarVarToTExp(TVarToTScalarVar(e1 : Var)),i : Int), Mul(TScalarVarToTExp(TVarToTScalarVar(e2 : Var)), j : Int)) 
			if (ltS(j,i).isDefined)
				=> Add(Mul(TScalarVarToTExp(TVarToTScalarVar(e2)),j),Mul(TScalarVarToTExp(TVarToTScalarVar(e1)),i))
		case Add(Add(TScalarVarToTExp(TVarToTScalarVar(e : Var)), Mul(TScalarVarToTExp(TVarToTScalarVar(e1 : Var)), i : Int)),Mul(TScalarVarToTExp(TVarToTScalarVar(e2 : Var)), j : Int)) 
			if (ltS(j,i).isDefined)
				=> Add(Add(TScalarVarToTExp(TVarToTScalarVar(e)), Mul(TScalarVarToTExp(TVarToTScalarVar(e2)), j)),Mul(TScalarVarToTExp(TVarToTScalarVar(e1)), i)) 
	}

	/*
	 * Port of CombineMul rule
	 */
	def CombineMul = rulefs {
		// Combine shared multipliers
 	 	// CombineMul : |[ e1 * i + e2 * i ]| -> |[ (e1 + e2) * i ]|           where <not(?"1")>i
 	 	// CombineMul : |[ e + e1 * i + e2 * i ]| -> |[ e + (e1 + e2) * i ]|   where <not(?"1")>i
		case Add(Mul(TScalarVarToTExp(TVarToTScalarVar(e1 : Var)),i : Int), Mul(TScalarVarToTExp(TVarToTScalarVar(e2 : Var)), j : Int)) 
			if (i != Int("1") && j == i)
				=> Mul(Add(TScalarVarToTExp(TVarToTScalarVar(e1)),TScalarVarToTExp(TVarToTScalarVar(e2))), i)
		case Add(Add(TScalarVarToTExp(TVarToTScalarVar(e : Var)), Mul(TScalarVarToTExp(TVarToTScalarVar(e1 : Var)), i : Int)),Mul(TScalarVarToTExp(TVarToTScalarVar(e2 : Var)), j : Int)) 
			if (i != Int("1") && j == i)
				=> Add(TScalarVarToTExp(TVarToTScalarVar(e)),Mul(Add(TScalarVarToTExp(TVarToTScalarVar(e1)),TScalarVarToTExp(TVarToTScalarVar(e2))),i))
	}


	/*
	 * Port of EliminateMul1 rules
	 */
	def EliminateMul1 = rulefs {
		// Eliminate unit multiplier
 	 	// EliminateMul1 : |[ e * 1 ]|          -> |[ e ]|
 	 	// EliminateMul1 : |[ e * -1 ]|         -> |[ -e ]|
		case Mul(TScalarVarToTExp(TVarToTScalarVar(e : Var)),Int("1"))
			=> TScalarVarToTExp(TVarToTScalarVar(e))
		case Mul(TScalarVarToTExp(TVarToTScalarVar(e : Var)),Int("-1"))
			=> Neg(TScalarVarToTExp(TVarToTScalarVar(e)))
	}
	
	private def falseStrategy : Strategy = rulefs { case _ => False() }
	private def trueStrategy : Strategy = rulefs { case _ => True() }
}